(THVSETQ (THV BT)NIL)
(THVSETQ(THV TXV)NIL)


(DEFPROP INCGCTR
   (LAMBDA(B)
      (PROG ()
	(COND((AND(EQ @THCONSE(CAR B))(THV WF))
	      (THSETQ(THV GCTR)(ADD1(THV GCTR)))))
	(RETURN T)  ))
EXPR)


(DEFPROP TRACEBIND
   (LAMBDA(TX TY)
      (PROG(BX BY TXX TTL)
	(COND((NOT(AND(THV WF)BTSW(THV TXV)))(RETURN NIL)))
	(COND((THVAR(CAR(THV TXV)))(SETQ TXX(CAR(THV TXV))))
	     (T(SETQ TXX TX)))
	(COND((THVAR TY)(SETQ BY(CADR(THGAL TY THALIST)))))
	(COND((THVAR TXX)(SETQ BX(CADR(THGAL TXX THOLIST)))))
	(COND(BY(GO TR5))
	     ((EQ BX @THUNASSIGNED)(GO TR3))
	     (T(GO TR6)))
TR3	(SETQ TTL(FINDTL(LIST(CADR TXX)(THV LCTR))T(THV BT)))
	(COND(TTL(THSETQ(THV BT)(CONS(CONS(LIST(LIST(CADR TXX)(THV LCTR))TY)TTL)(THV BT))))
	     (T(GO TR6)))
	(SETQ TTL(FINDTL TY NIL(THV BT)))
	(COND(TTL(THSETQ(THV BT)(CONS(CONS(LIST(LIST(CADR TXX)(THV LCTR))TY)TTL)(THV BT))))
	     (T(THSETQ(THV BT)(CONS(LIST(LIST(LIST(CADR TXX)(THV LCTR))TY))(THV BT)))))
	(GO TR6)
TR5	(COND((NOT(EQ BY @THUNASSIGNED))(GO TR6))
	     ((NOT BX)(GO TR4))
	     ((EQ BX @THUNASSIGNED)(GO TR2)) )
TR1	(SETQ TTL(FINDTL(LIST(CADR TXX)(NTHV @LCTR 1 THALIST))T(THV BT)))
	(COND(TTL(THSETQ(THV BT)(CONS(APPEND(LIST(LIST(LIST(CADR TY)(ADD1(THV GCTR)))BX)
						 (LIST(LIST(CADR TY)(ADD1(THV GCTR)))(LIST(CADR TXX)(NTHV @LCTR 1 THALIST))))
					     TTL)(THV BT) )))
	     (T(THSETQ(THV BT)(CONS(LIST(LIST(LIST(CADR TY)(ADD1(THV GCTR)))BX)
					(LIST(LIST(CADR TY)(ADD1(THV GCTR)))(LIST(CADR TXX)(NTHV @LCTR 1 THALIST)))
					(LIST(LIST(CADR TXX)(NTHV @LCTR 1 THALIST))BX))(THV BT)))))
	(GO TR6)
TR2	(SETQ TTL(FINDTL(LIST(CADR TXX)(NTHV @LCTR 1 THALIST))T(THV BT)))
	(COND(TTL(THSETQ(THV BT)(CONS(CONS(LIST(LIST(CADR TY)(ADD1(THV GCTR)))(LIST(CADR TXX)(NTHV @LCTR 1 THALIST)))
					  TTL)(THV BT))))
	     (T(THSETQ(THV BT)(CONS(LIST(LIST(LIST(CADR TY)(ADD1(THV GCTR)))(LIST(CADR TXX)(NTHV @LCTR 1 THALIST))))
				    (THV BT)))))
	(GO TR6)
TR4	(THSETQ(THV BT)(CONS(LIST(LIST(LIST(CADR TY)(ADD1(THV GCTR)))TXX))(THV BT)))
TR6	(THSETQ(THV TXV)(CDR(THV TXV)) T T)
	(RETURN NIL)   ))
EXPR)




(DEFPROP FINDTL
  (LAMBDA(E FS B)
	(COND((NULL B)NIL)
	     ((AND FS(EQUAL E(CAAAR B)))(CAR B))
	     ((AND(NOT FS)(EQUAL E(CADAAR B))(NOT(NUMBERP(CADR(EXPLODE(CAAAAR B))))))(CAR B))
	     (T(FINDTL E FS(CDR B))))   )
EXPR)





(DEFPROP SAVAR
   (LAMBDA(THA1)
      (PROG NIL
	(COND((AND(NULL SSW) CT)(RPLACA(CAR CT)(CONS(COND((ATOM(CAAR CT))(CAAR CT))(T(CAAAR CT)))(LIST THA2)))))
	(COND((AND(THV WF)BTSW(NOT(NUMBERP THA1)))(THSETQ(THV TXV)(MAPCAR(FUNCTION ETHEV)THA1))))   ))
EXPR)


(DEFPROP SIMPLE
   (LAMBDA(THA2B)
	(COND((NULL SRULES)THA2B) 
	     ((NULL THA2B)NIL)
	     ((OR(ATOM(CAR THA2B))(EQ @THV(CAAR THA2B)))
	      (CONS(CAR THA2B)(SIMPLE(CDR THA2B))))
	     (T(CONS(SIMPLE1(CAR THA2B))(SIMPLE(CDR THA2B))))))
EXPR)


(DEFPROP SIMPLE1
   (LAMBDA(X)
      (PROG(TX TR)
	(SETQ TR SRULES)
	(SETQ TX X)
SI3	(SETQ TX(SIMPLE2 TX(CAR TR)))
	(SETQ TX(SIMPLE2 TX(CAR TR)))
	(SETQ TR(CDR TR))
	(COND(TR (GO SI3)))
	(RETURN TX)  ))
EXPR)


(DEFPROP SIMPLE2
   (LAMBDA(X R)
	(COND((OR(ATOM X)(EQ @THV(CAR X))(AND(EQ @#(CAR X))
					   (OR(ATOM(CADDR X))(NULL(CDADDR X))))(NULL(CDR X)))X)
	     ((AND(NULL(CDDR X))(EQ(CAR X)(CAAR R))(NOT(OR(ATOM(CADR X))(NULL(CADADR X))))(EQ(CAADR X)(CAADAR R)))
	      (COND((ATOM(CADR R))(SIMPLE2(CADADR X)R))
		   (T(CONS(CAADR R)(LIST(SIMPLE2(CADADR X)R))))))
	     ((AND(EQ(CAR X)(CAAR R))(EQ @#(CAADR X))(NOT(ATOM(CADDAR(CDR X))))(EQ(CAADDR(CADR X))(CAADAR R)))
	      (COND((ATOM(CADR R))(SIMPLE2(CADADR(CDADR X))R))(T(CONS(CAADR R)(LIST(SIMPLE2(CADADR(CDADR X))R))))))
	     ((AND(EQUAL(CAR X)(CAAR R))(NOT(ATOM(CADR X)))(CDDAR R)(CDDR X)
	          (EQUAL(CAADR X)(CAADAR R))(EQUAL(CAR(CDDADR X))(CADDR X)))
	      (CADADR X))
	     ((CDDR X) X)
	     (T(CONS(CAR X)(LIST(SIMPLE2(CADR X)R))))))
EXPR)

(DEFPROP ETHEV
   (LAMBDA(ATHA1)
	(COND((EQ(CAR ATHA1)@THEV)(THVAL(CADR ATHA1)THALIST))
	     (T ATHA1))  )
EXPR)



(DEFPROP NTHV
   (LAMBDA(K N L)
	(COND((NULL L)(PRINT @LCTR_NOT_BOUND))
	     ((AND(EQ K(CAAR L))(ZEROP N))(CADAR L))
	     ((EQ K(CAAR L))(NTHV K(SUB1 N)(CDR L)))
	     (T(NTHV K N(CDR L))))  )
EXPR)


(DEFPROP COLLECTDB
   (LAMBDA(THY)
	(COND((AND (THV ULS)THY(NULL SSW)CT 
		   (NOT(SUBSTP(CDAR CT)(CADR THE))))
	      (COND((EQ @IF(CADAR CT))
                    (RPLACA CT(CONS(CAAR CT)(APPEND(CONSIFL(CDAR CT))(APPEND(FIXBADDBMATCH(CADR THE)THY)
						     (CDRIFL(CDAR CT)))))) )
		   (T(RPLACA CT(CONS(CAAR CT)(APPEND(FIXBADDBMATCH(CADR THE)THY)
						     (CDAR CT)))))))
  	     ((AND(THV ULS)THY(NULL SSW)CT)
	      (COND((EQ @IF(CADAR CT))
		    (RPLACA CT(CONS(CAAR CT)(APPEND(CONSIFL(CDAR CT))(UPDATLIT(CDRIFL(CDAR CT))(CADR THE)
										  (LIST(THVARSUBST(CADR THE))))))))
		   (T(RPLACA CT(CONS(CAAR CT)(UPDATLIT(CDAR CT)(CADR THE)(LIST(THVARSUBST(CADR THE)))))))))))
EXPR)



(DEFPROP CONSIFL
   (LAMBDA(IFL)
	(COND((NULL IFL)NIL)((ATOM(CAR IFL))(CONS @IF(CONSIFL(CDR IFL))))
	     (T NIL))   )
EXPR)


(DEFPROP CDRIFL
   (LAMBDA(IFL)
      	(COND((NULL IFL)NIL)((ATOM(CAR IFL))(CDRIFL(CDR IFL)))
	     (T IFL))  )
EXPR)




(DEFPROP FIXBADDBMATCH
   (LAMBDA(CTHE CTHY)
      (PROG(TTHY)
	(SETQ TTHY(FIXDB1(THVARSUBST CTHE)CTHY))
	(COND((NULL TTHY)(RETURN NIL)))
	(RETURN(LIST(CONS CTHE TTHY)))   ))
EXPR)


(DEFPROP FIXDB1
   (LAMBDA(VTHE VTHY)
	(COND((NULL VTHY)NIL)
	     ((OR(SUBSTP VTHE @THV)(EQUAL VTHE(CAAR VTHY)))VTHY)
	     (T(FIXDB1 VTHE(CDR VTHY))))   )
EXPR)




(DEFPROP UPDATLIT
   (LAMBDA(GHITS X Y)
	(COND((NULL GHITS)NIL)
	     ((EQUAL X(CAAR GHITS))
	      (APPEND(UPDATLIT1(CAAR GHITS)(CDAR GHITS)Y)(CDR GHITS)))
	     (T(CONS(CAR GHITS)(UPDATLIT(CDR GHITS)X Y))))  )
EXPR)


(DEFPROP UPDATLIT1
   (LAMBDA(GTHE AGHITS Y)
	(COND((NULL AGHITS)NIL)
	     ((EQUAL Y(CAR AGHITS))
	      (LIST(CONS GTHE AGHITS)))
	     (T(UPDATLIT1 GTHE(CDR AGHITS)Y)))  )
EXPR)


(DEFPROP STEPT
   (LAMBDA NIL
	(COND((AND 
		(NOT(EQ(CAR THE)@THASSERT))
		THVALUE
		(NULL SSW)
		CT
		(CDAR CT)
		(OR
			(EQUAL THE @(THFAIL))
			(AND
				(EQ(CAR THE)@THGOAL)
				(NOT(EQUAL(THVARSUBST(CADR THE))(CAR THVALUE)))))
		(NOT(ATOM(CADADR THTREE)))
		(ATOM(CAR(CADADR THTREE))))
	      (COND((EQ @IF(CADAR CT))
		    (RPLACA CT(CONS(CAAR CT)(APPEND(CONSIFL(CDAR CT))(UPDATLIT(CDRIFL(CDAR CT))(CADADR THTREE)THVALUE)))))
		   (T(RPLACA CT(CONS(CAAR CT)(UPDATLIT(CDAR CT)(CADADR THTREE)THVALUE))))))))
EXPR)